% RA: Relación 02
% OTTER: granjero.in
% Departamento de Ciencias de la Computación e Inteligencia Artificial
%==============================================================================


%==============================================================================
% Enunciado
%==============================================================================

% En la orilla de un río hay un granjero con una caja de coles, una oveja y un
% lobo. El granjero quiere pasar a la otra orilla con todas sus cosas y para
% ello dispone de una barca en la que, como mucho, caben dos elementos. Por
% otro lado, el granjero ha de evitar dejar sólos en una orilla a la oveja con
% las coles (pues perdería las coles) o al lobo con la oveja (pues perdería la
% oveja). Determinar qué secuencia de desplazamientos de una orilla a otra
% tiene que realizar el granjero para pasar a la otra orilla con todas sus
% cosas.

% Utilizar OTTER para encontrar una solución al problema.

%==============================================================================
% Formalización
%==============================================================================

make_evaluable(_-_,$DIFF(_,_)).
assign(max_proofs,-1).

set(hyper_res).
set(ur_res).
set(very_verbose).

formula_list(sos).
  all x1 x2 x3 x4 w
    ((orilla(l,x2,x3,x4,$IGNORE(w)) & 
      x2 != x3 & x3 != x4) ->
     orilla(r,x2,x3,x4,$IGNORE(["El granjero va solo"|w]))).

  all x1 x2 x3 x4 w
    ((orilla(r,x2,x3,x4,$IGNORE(w)) & 
      x2 != x3 & x3 != x4) ->
     orilla(l,x2,x3,x4,$IGNORE(["El granjero vuelve solo"|w]))).

% Si las orillas del río se identifican con 0 y 1, entonces se pueden unificar
% las dos fórmulas anteriores en la siguiente, indicando que '-' es un símbolo
% asociado al operador evaluable de resta ($DIFF)

%  all v x1 x2 x3 x4 w ((orilla(v,x2,x3,x4,$IGNORE(w)) & 
%                      x2 != x3 & x3 != x4) ->
%                      orilla(1-v,x2,x3,x4,$IGNORE(["El granjero va solo"|w]))).

  all x1 x2 x3 x4 w
    ((orilla(l,l,x3,x4,$IGNORE(w)) & 
      x3 != x4) ->
     orilla(r,r,x3,x4,$IGNORE(["El granjero va con el lobo"|w]))).

  all x1 x2 x3 x4 w
    ((orilla(r,r,x3,x4,$IGNORE(w)) & 
      x3 != x4) ->
     orilla(l,l,x3,x4,$IGNORE(["El granjero vuelve con el lobo"|w]))).

  all x1 x2 x3 x4 w
    (orilla(l,x2,l,x4,$IGNORE(w)) ->
     orilla(r,x2,r,x4,$IGNORE(["El granjero va con la oveja"|w]))).

  all x1 x2 x3 x4 w
    (orilla(r,x2,r,x4,$IGNORE(w)) ->
     orilla(l,x2,l,x4,$IGNORE(["El granjero vuelve con la oveja"|w]))).

  all x1 x2 x3 x4 w
    ((orilla(l,x2,x3,l,$IGNORE(w)) & 
      x2 != x3) ->
     orilla(r,x2,x3,r,$IGNORE(["El granjero va con la col"|w]))).

  all x1 x2 x3 x4 w
    ((orilla(r,x2,x3,r,$IGNORE(w)) & 
      x2 != x3) ->
     orilla(l,x2,x3,l,$IGNORE(["El granjero vuelve con la col"|w]))).

  l != r.
  r != l.

  orilla(l,l,l,l,$IGNORE([])).
end_of_list.

% La segunda solución queda subsumida por la primera y por eso no aparece.

formula_list(passive).
  all w (orilla(r,r,r,r,$IGNORE(w)) -> $ANS(w)).
end_of_list.

%==============================================================================
